Abstract Binding Trees

ABTs enrich Abstract Syntax Trees with the means to introduce new variables and symbols, called a binding, with a specified range of significance, called its scope.

The scope of a binding is the ABT within which the bound identifier can be used. The crucial principle is that any use of an identifier should be understood as a reference to its binding.

An argument to an operator is called an abstractor, and has the form $x_1, ...,x_k .a$ where the $x$s are variables bound within the ABT $a$.